A:Type, I:MaInterface(A), i:{i:Id| (i  fpf-domain(I))} . (I(i).2)  k:Knd fp Top 

latex

Definitions	x:A. B(x), t  T, a:A fp B(a), P  Q, S  T, Top,
Lemmas	Id wf, l member wf, fpf-domain wf, ma-interface wf, ma-interface-da-type0, Knd wf, assert wf, hasloc wf, top wf, subtype rel function, subtype-set-hasloc, ma-interface-type-trivial